Section: New Results

Virtual Machine

Participants : Olivier Gruber, Fabienne Boyer, Damien Pous, Ludovic Demontes, Clément Deschamps.

A core aspect of the Synergy virtual machine is its ability to reconfigure component-based applications at execution time. We have focused on the reconfiguration protocol with the intent of verifying and proving its robustness.

In a first step, we have formalized and verified that any correct and complex reconfiguration through our reconfiguration protocol can be processed as a sequence of elementary reconfiguration operations and always results in a component assembly that is architecturally consistent. This aspect has been verified using model-checking techniques. This work has been done in collaboration with Gwen Salaün from the VASY team (Inria Rhône-Alpes). It lead to a publication in the Formal Method (FM'11) conference [30] .

In a second step, we have considered software failures that may occur during a reconfiguration. Although the protocol is trusted code, it invokes components to reconfigure them, thereby executing unsafe code that may fail. This work with Damien Pous produced a high-level formalisation of our reconfiguration protocol and a completely certified modelisation of these algorithms in Coq [50] . This work resulted in a submitted publication.

Finally, we have also investigated the control of complex reconfiguration through using discrete synchronous control techniques with Eric Rutten and Gwenael Delaval [44] .